package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import com.microsoft.z3.Z3Exception;

import ast.ActsFor;
import ast.AndPredicate;
import ast.Assert;
import ast.Binder;
import ast.Call;
import ast.Case;
import ast.ChannelConstant;
import ast.CompositeBinder;
import ast.Constant;
import ast.Dummy;
import ast.ExistsPredicate;
import ast.ExpVar;
import ast.Expression;
import ast.ForallPredicate;
import ast.Go;
import ast.In;
import ast.Label;
import ast.None;
import ast.NumPredicate;
import ast.OrPredicate;
import ast.Out;
import ast.ParallelProcess;
import ast.PrefixedProcess;
import ast.Procedure;
import ast.Process;
import ast.NewConstP;
import ast.QualityPredicate;
import ast.Some;
import ast.Term;

public class ProcessJudgement extends FLJudgement {
	
	private Process process;
	private HashMap<String, HashSet<Term>> kappa;
	private BoolExpr varphi;
	private PsiNode psi;
	
	public ProcessJudgement(
			Process p,
			HashMap<String, HashSet<Term>> rho,
			HashMap<String, HashSet<Term>> kappa, 
			BoolExpr varphi)
	{
		process = p;
		setRho(rho);
		this.kappa = kappa;
		this.varphi = varphi;
		psi = new PsiNode();
	}
	
	public ProcessJudgement(
			Process p,
			HashMap<String, HashSet<Term>> rho,
			HashMap<String, HashSet<Term>> kappa, 
			BoolExpr varphi, 
			PsiNode psi)
	{
		this(p, rho, kappa, varphi);
		this.psi = psi;
	}
	
	public HashMap<String, HashSet<Term>> getKappa() 
	{
		return kappa;
	}
	
	public BoolExpr getVarphi()
	{
		return varphi;
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public String toString()
	{
		String res = "";
		res += "rho, kappa |- " + "(" + varphi + ")" + 
					process.toString(0) + ":" + psi;
		return res;
	}
	
	public ArrayList<DischargeResult> discharge() throws Z3Exception
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		
		Context ctx = FLAnalysis.getCtx();
		Solver solver = FLAnalysis.getSolver();
		
		if (process instanceof NewConstP) {
			
			Constant c = ((NewConstP) process).getConstant();
			if (c instanceof ChannelConstant) {
				Label lb = ((ChannelConstant) c).getLabel();
				LabelJudgement lbjgt = new LabelJudgement(lb);
				resList.add(new Inclusion(lbjgt.getPsi(), psi, true));
			}
			
			ProcessJudgement pjgt = new ProcessJudgement(
					((NewConstP) process).getProcess(), getRho(), kappa, varphi);
			resList.add(pjgt);
			resList.add(new Inclusion(pjgt.getPsi(), psi, true));
			
		} else if (process instanceof ParallelProcess) {
			
			ProcessJudgement pjgt = null;
			for (Process curProc : ((ParallelProcess) process).getProcesses()) {
				pjgt = new ProcessJudgement(curProc, getRho(), kappa, varphi);
				resList.add(pjgt);
				resList.add(new Inclusion(pjgt.getPsi(), psi, true));
			}
			
		} else if (process instanceof Go) {
			
			ProcessJudgement pjgt = new ProcessJudgement(
					((Go) process).getProcess(), getRho(), kappa, varphi);
			resList.add(pjgt);
			resList.add(new Inclusion(pjgt.getPsi(), psi, true));
			
			TermJudgement tjgt = new TermJudgement(((Go) process).getTerm(), getRho());
			HashSet<Node> stSet = new HashSet<Node>();
			stSet.add(SiteTp.getInstance());
			HashSet<Node> srtSet = new HashSet<Node>();
			srtSet.add(SrtSignal.getInstance());
			HashSet<Node> vSet = new HashSet<Node>();
			vSet.add(new FreeVariable("#v"));
			Constraint guard = new Negation(
					new ForallConstraint(
							new BoundVariable("#v"), 
							tjgt.getRes(), 
							new Inclusion(new ConcreteSetNode(vSet), new ConcreteSetNode(stSet), false)));
			GuardedConstraint gc = new GuardedConstraint(
					guard,	
					new Inclusion(new ConcreteSetNode(srtSet), psi, true));
			resList.add(gc);
			
		} else if (process instanceof PrefixedProcess) {
			
			Binder b = ((PrefixedProcess) process).getBinder();
			BinderJudgement bdjgt = new BinderJudgement(b, getRho());
			resList.add(bdjgt);
			resList.add(new Inclusion(bdjgt.getPsi(), psi, true));
			
			solver.push();
			BoolExpr newVarphi = ctx.mkAnd(varphi, getAvaFormulaOfBinder(b));
			solver.add(newVarphi);
			if (solver.check() == Status.SATISFIABLE) {
				ProcessJudgement pjdgt = new ProcessJudgement(
					((PrefixedProcess) process).getProcess(), getRho(), kappa, newVarphi);
				resList.add(pjdgt);
				resList.add(new Inclusion(pjdgt.getPsi(), psi, true));
			} 
			solver.pop();
			
		} else if (process instanceof Call) {
			
			ArrayList<Expression> args = ((Call) process).getArguments();
			ExpressionJudgement ejdgt = null;
			Procedure callee = STSimplifier.getProcedureMap().get(
					((Call) process).getName());
			for (int i = 0; i < args.size(); i++) {
				Expression arg = args.get(i);
				ejdgt = new ExpressionJudgement(arg, getRho());
				resList.add(ejdgt);
				resList.add(new Inclusion(ejdgt.getPsi(), psi, true));
				String formalParName = callee.getParams().get(i).getName();
				// for the i-th argument and parameter we use v_{i+1} as bound variable
				// in the universal quantification
				HashSet<Node> vSet = new HashSet<Node>();
				vSet.add(new FreeVariable("#v" + (i + 1)));
				resList.add(new ForallConstraint(
								new BoundVariable("#v" + (i + 1)),
								ejdgt.getRes(),
								new Inclusion(new ConcreteSetNode(vSet), 
											  new RhoNode(new FreeVariable(formalParName)),
											  true)));
			}
			
		} else if (process instanceof Dummy) {
			
			ProcessJudgement pjdgt = new ProcessJudgement(
					((Dummy) process).getProcess(), getRho(), kappa, varphi);
			resList.add(pjdgt);
			resList.add(new Inclusion(pjdgt.getPsi(), psi, true));
			HashSet<Node> rcSet = new HashSet<Node>();
			rcSet.add(RcSignal.getInstance());
			resList.add(new Inclusion(new ConcreteSetNode(rcSet), psi, true));
			
		} else if (process instanceof Case) {
			
			Expression e = ((Case) process).getE();
			ExpressionJudgement ejdgt = new ExpressionJudgement(e, getRho());
			resList.add(ejdgt);
			resList.add(new Inclusion(ejdgt.getPsi(), psi, true));
			
			// ne(rho(e))\subseteq rho(y)
			HashSet<Node> neVSet = new HashSet<Node>();
			neVSet.add(new FreeVariable("#v"));
			FreeVariable y = new FreeVariable(((Case) process).getY().getName());
			resList.add(new ForallConstraint(
							new BoundVariable("#v"),
							ejdgt.getRes(),
							new Inclusion(new ConcreteSetNode(neVSet),
										  new RhoNode(y), true)));
			
			// two branches
			solver.push();
			BoolExpr newVarphi1 = ctx.mkAnd(varphi, getAvaFormulaOfExpr(e));
			solver.add(newVarphi1);
			if (solver.check() == Status.SATISFIABLE) {
				ProcessJudgement p1jdgt = new ProcessJudgement(
						((Case) process).getProcess1(), getRho(), kappa, newVarphi1);
				resList.add(p1jdgt);
				resList.add(new Inclusion(p1jdgt.getPsi(), psi, true));
			}
			solver.pop();
			
			solver.push();
			BoolExpr newVarphi2 = ctx.mkAnd(varphi, ctx.mkNot(getAvaFormulaOfExpr(e)));
			solver.add(newVarphi2);
			if (solver.check() == Status.SATISFIABLE) {
				ProcessJudgement p2jdgt = new ProcessJudgement(
						((Case) process).getProcess2(), getRho(), kappa, newVarphi2);
				resList.add(p2jdgt);
				resList.add(new Inclusion(p2jdgt.getPsi(), psi, true));
			}
			solver.pop();
			
		} else if (process instanceof ActsFor) {
			
			ProcessJudgement p1jdgt = new ProcessJudgement(
					((ActsFor) process).getProcess1(), getRho(), kappa, varphi);
			ProcessJudgement p2jdgt = new ProcessJudgement(
					((ActsFor) process).getProcess2(), getRho(), kappa, varphi);
			resList.add(p1jdgt);
			resList.add(p2jdgt);
			resList.add(new Inclusion(p1jdgt.getPsi(), psi, true));
			resList.add(new Inclusion(p2jdgt.getPsi(), psi, true));
			
			TermJudgement[] tjdgts = new TermJudgement[2];
			tjdgts[0] = new TermJudgement(((ActsFor) process).getT1(), getRho());
			tjdgts[1] = new TermJudgement(((ActsFor) process).getT2(), getRho());
			for (int i = 0; i < 2; i++) {
				resList.add(tjdgts[i]);
				resList.add(new Inclusion(tjdgts[i].getPsi(), psi, true));
				
				HashSet<Node> srtSet = new HashSet<Node>();
				srtSet.add(SrtSignal.getInstance());
				HashSet<Node> prSet = new HashSet<Node>();
				prSet.add(PrincipalTp.getInstance());
				HashSet<Node> vSet = new HashSet<Node>();
				vSet.add(new FreeVariable("#v"));
				resList.add(new GuardedConstraint(
						new Negation(new ForallConstraint(
										new BoundVariable("#v"),
										tjdgts[i].getRes(),
										new Inclusion(
												new ConcreteSetNode(vSet), 
												new ConcreteSetNode(prSet), false))),
						new Inclusion(new ConcreteSetNode(srtSet), psi, true)));
			}
			
		} else {
			// the process is 0 and no constraint needs to be generated
		}
		
		return resList;
	}
	
	private BoolExpr getAvaFormulaOfExpr(Expression e) throws Z3Exception
	{
		BoolExpr res = null;
		Context ctx = FLAnalysis.getCtx();
		
		if (e instanceof Some) {
			res = ctx.mkTrue();
		} else if (e instanceof None) {
			res = ctx.mkFalse();
		} else if (e instanceof ExpVar){
			res = ctx.mkBoolConst(((ExpVar) e).getName());
		}
		
		return res;
	}
	
	private BoolExpr getAvaFormulaOfBinder(Binder b) throws Z3Exception
	{
		BoolExpr res = null;
		Context ctx = FLAnalysis.getCtx();
		
		if (b instanceof In) {
			
			res = ctx.mkBoolConst(((In) b).getX().getName());
			
		} else if (b instanceof Out) {
			
			res = ctx.mkTrue();
			
		} else if (b instanceof CompositeBinder) {
			
			QualityPredicate pred = ((CompositeBinder) b).getQ();
			res = getAvaFormulaFromPredicate(b, pred);
			
		} else if (b instanceof Assert) {
			
			res = getAvaFormulaOfBinder(((Assert) b).getBinder());
		}
		
		return res;
	}
	
	private BoolExpr getAvaFormulaFromPredicate(
			Binder b, QualityPredicate pred) throws Z3Exception {
		
		BoolExpr res = null;
		Context ctx = FLAnalysis.getCtx();

		if (pred instanceof AndPredicate) {
			
			int size = ((AndPredicate) pred).getOps().size();
			BoolExpr[] args = new BoolExpr[size];
			for (int i = 0; i < size; i++) {
				args[i] = getAvaFormulaFromPredicate(b,
						((AndPredicate) pred).getOps().get(i));
			}
			res = ctx.mkAnd(args);
			
		} else if (pred instanceof OrPredicate) {
			
			int size = ((OrPredicate) pred).getOps().size();
			BoolExpr[] args = new BoolExpr[size];
			for (int i = 0; i < size; i++) {
				args[i] = getAvaFormulaFromPredicate(b, 
						((OrPredicate) pred).getOps().get(i));
			}
			res = ctx.mkOr(args);
					
		} else if (pred instanceof ForallPredicate) {
			
			int size = ((CompositeBinder) b).getComponentBinders().size();
			BoolExpr[] args = new BoolExpr[size];
			for (int i = 0; i < size; i++) {
				args[i] = getAvaFormulaOfBinder( 
						((CompositeBinder) b).getComponentBinders().get(i));
			}
			res = ctx.mkAnd(args);
			
		} else if (pred instanceof ExistsPredicate) {
			
			int size = ((CompositeBinder) b).getComponentBinders().size();
			BoolExpr[] args = new BoolExpr[size];
			for (int i = 0; i < size; i++) {
				args[i] = getAvaFormulaOfBinder( 
						((CompositeBinder) b).getComponentBinders().get(i));
			}
			res = ctx.mkOr(args);
			
		} else if (pred instanceof NumPredicate) {
			
			int bdIndex = ((NumPredicate) pred).getNum();
			// method guaranteed to receive a composite binder "b" when called
			// and "b" is not "decomposed" when calling ourselves
			res = getAvaFormulaOfBinder(
					((CompositeBinder) b).getComponentBinders().get(bdIndex - 1)); 
		}
		
		return res;
	}
}
